g:GrpSig, s:(|g|), a, b:|g|. a  b (mod s in g)   

latex

Up	groups 1
Definitions of Statement	a  b (mod s in g)
Definitions	x f y, a  b (mod s in g), t  T, , x:A. B(x)
Lemmas	grp sig wf, grp car wf, grp inv wf, grp op wf